Nuprl Lemma : as_strong_transitivity
4,23
postcript
pdf
T
:Type,
P
,
Q
,
R
:(
T
Prop).
P
as strong as
Q
Q
as strong as
R
P
as strong as
R
latex
Definitions
P
as strong as
Q
,
Prop
,
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
origin
T:Type, P, Q, R:(T
Prop). P as strong as Q 
Q as strong as R P as strong as R T:Type, P, Q, R:(TProp). P as strong as Q Q as strong as R P as strong as R 
Tx:A. B(x) Q